% This is LLNCS.DEM the demonstration file of
% the LaTeX macro package from Springer-Verlag
% for Lecture Notes in Computer Science,
% version 2.3 for LaTeX2e
%
\documentclass[orivec]{llncs}
%
%\usepackage{makeidx}  % allows for indexgeneration

\usepackage[english]{babel}
\usepackage[T1]{fontenc}

\usepackage{amsmath}
\usepackage{amssymb}
%\usepackage{amsthm}
%\usepackage{amslatex} 
\usepackage{amsfonts}
\usepackage{subfigure}
\usepackage{graphicx}
\usepackage{xspace}
\usepackage{times}

\usepackage{ifthen}
\usepackage{url}
\usepackage{mathpartir}

% This refers to japerez.sty, the file with the commands that I wrote.
\usepackage{japerez}
% Davides's macro
\usepackage{davidemacro} 
\usepackage{evolvablemacro}


\usepackage{myproof}
%\usepackage{xytree}



%\newcommand{\mma}{Minsky machine\xspace}
%\newcommand{\hide}[1]{}
%\newcommand{\ahopi}{\ensuremath{\textsc{Ho}^{-\mathsf{f}}}\xspace}
%\newcommand{\hocore}{\ensuremath{\textsc{Hocore}}\xspace}
\newcommand{\hop}{\ensuremath{\textsc{Ho}^{\textsc{P}}\xspace}}

\newcommand{\ambient}{\ensuremath{\textsc{Amb}}\xspace}



% Notation for passivation units and ambients
\newcommand{\pu}[2]{\ensuremath{#1\{#2\}}}
\newcommand{\ambi}[2]{\ensuremath{#1[#2]}}
\newcommand{\openamb}[1]{\ensuremath{\mathtt{open}\, #1}}
\newcommand{\inamb}[1]{\ensuremath{\mathtt{in}\, #1}}
\newcommand{\outamb}[1]{\ensuremath{\mathtt{out}\, #1}}
\newcommand{\eatamb}[1]{\ensuremath{\mathtt{pull}\, #1}}
\newcommand{\expelamb}[1]{\ensuremath{\mathtt{push}\, #1}}
\newcommand{\new}[2]{ \nu\, #1\, (#2)}

\newcommand{\names}[1]{\mathtt{names}_{#1}}
\newcommand{\manager}[1]{\mathtt{Manager}_{#1}}


\pagestyle{plain}


%\newcommand{\Ho}[2]{\overline{#1} \langle #2 \rangle}
\newcommand{\blockout}[2]{\ensuremath{\Ho{#1}{#2}}}


\newcommand{\shortv}[1]{}%{#1}
\newcommand{\longv}[1]{#1}


%\newcommand{\delim}[1]{\subsubsection*{#1}}
\newcommand{\delim}[1]{\noindent {\bf{#1}}~}
\newcommand{\delimit}[1]{\noindent {\emph{#1}}~}

%% Height
%\addtolength{\voffset}{-0.8cm} 
%\addtolength{\textheight}{1.7cm} 
%% Width
%\addtolength{\hoffset}{-0.6cm}
%\addtolength{\textwidth}{1.2cm} 

%\usepackage{hyperref}
%

\renewcommand{\vspace}[1]{}
%\renewcommand{\small}{}
\begin{document}
%

%
\mainmatter              % start of the contributions
%

\title{On the Expressiveness of Adaptable Processes \\ (Draft of \today)}
 \author{... \and Cinzia Di Giusto\inst{1}   \and Jorge A. P\'erez\inst{2} \and Alan Schmitt\inst{1} \and ...}
\institute{INRIA Grenoble - Rh\^one Alpes
\and FCT New University of Lisbon}
%
%\authorrunning{Cinzia Di Giusto et al.}   % abbreviated author list (for running head)
%
%%%% list of authors for the TOC (use if author list has to be modified)

%

\maketitle              % typeset the title of the contribution
%\begin{abstract} Bla \end{abstract}
%

\begin{abstract}
The abstract
\end{abstract}

\section{Preliminaries}
The $\mathcal{E}$ calculus %in the sequel) 
is a variant of CCS \cite{Milner89} without restriction and relabeling, 
and extended with constructs for evolvability. 
As in CCS, in $\mathcal{E}$ 
processes can perform actions or synchronize on them.  
We presuppose a countable
set $\mathcal{N}$ of names, ranged over by $a,b$, possibly decorated as 
$\overline{a},  \overline{b} \ldots $ and $\til{a}, \til{b} \ldots $. 
Also, we assume a countable set $\mathcal{X}$ of variables, ranged over $x,y,\ldots$.
As customary, we use $a$ and $\outC{a}$ to denote atomic input and output actions, respectively.
The syntax of $\mathcal{E}$ processes 
extends that of CCS with 
%is the following:
 primitive notions of \emph{adaptable processes} $\component{a}{P}$
 and \emph{update prefixes} $\update{a_{x}}{U}$:
 \[
P        ::=  \component{a}{P} \sepr 
          P \parallel P  \sepr \sum_{i \in I} \pi_i.P_i  \sepr ! \pi.P 
          \quad \quad \quad 
\pi   ::=  a \sepr \outC{a} \sepr \update{a_{x}}{U}
\]
Above, 
the $U$ in the update prefix
$\update{a_{x}}{U}$ ($x \in \mathcal{X}$) is an \emph{update pattern}: it represents   
a context, i.e., a process with zero or more \emph{named holes}, denoted $\bullet_{x}$ ($x \in \mathcal{X}$) . 
More precisely,  we have:
    \[
U        ::=  \bullet_{x} \sepr \component{a}{U} \sepr 
          U \parallel U  \sepr \sum_{i \in I} \pi_i.U_i  \sepr ! \pi.U 
\]
Intuitively, the idea to establish a correspondence between
the $x$ in $\update{a_{x}}{U}$ and the holes $\bullet_{x}$ inside $U$ (possibly none).
Notice that $U$ may also contain holes $\bullet_{y}$ for some $x \neq y$; 
based on the correspondence, as a result of an update involving $\update{a_{x}}{U}$, only holes $\bullet_{x}$ will be substituted.
This is formalized by the operational semantics, which is given as an LTS.
Given transition labels 
\[
\alpha    ::=  ~~ a \sepr \outC{a} \sepr \component{a}{P} \sepr \update{a_{x}}{U} \sepr \tau
\]
the LTS for \evol{}, denoted $\arro{~\alpha~}$,  
is defined by the rules in Figure \ref{fig:ltswithalpha}.

This way, for instance, $\update{a_{x}}{\update{b_{y}}{ \bullet_{x} \parallel \bullet_{y}} \parallel \bullet_{x}} \parallel \component{a}{P} \pired 
\update{b_{y}}{ P \parallel \bullet_{y}} \parallel P$.

\begin{figure}[t]
\linefigure
$$
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\inferrule[\rulename{Comp}]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}
\qquad 
%  \mathrm{\textsc{Upd}}~~~\update{a}{P_1}.P_2 \arro{\update{a}{P_1}}  P_2
%$$
%$$
\inferrule[\rulename{Sum}]{}{\sum_{i\in I} \pi_i.P_i \arro{~\pi_j~}  P_j  ~~(j \in I)}  
%\rightinfer	[\textsc{Rec}]
 %			{rec \,X.P \arro{\alpha} P}
 %			{P\sub{rec \, X.P}{X} \arro{\alpha} P'}
 %\quad
\qquad
\inferrule[\textsc{(Repl)}]{}{!\pi.P \arro{~\pi~}  P \parallel !\pi.P }
\quad
\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}
$$
$$
 \inferrule[\rulename{Act1}]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}			
\quad
\inferrule[\rulename{Tau1}]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}
\quad 
\inferrule[\rulename{Tau3}]{P_1 \arro{~\component{a}{Q}~} P_1'\andalso P_2 \arro{~\update{a_{x}}{U}~} P_2'}{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ U\sub{Q}{x}  }{\star} \parallel P_2'}
$$

\caption{LTS for \evols{} and \evold{}.
Rules \rulename{Act2}, \rulename{Tau2}, and \rulename{Tau4}---the symmetric counterparts of 
\rulename{Act1}, \rulename{Tau1}, and \rulename{Tau3}---have been omitted.} \label{fig:ltswithalpha}
%\end{table}
\linefigure
\end{figure}

\section{Encodings}
Two notions of encoding:
\begin{itemize}
 \item \emph{Paranoid:} There are no assumptions on the nature of contexts
 \item \emph{Gorla-like:} The context follows the ``rules'' of the encoding
\end{itemize}

\begin{mydefi}
\begin{enumerate}
 \item Compositional (in the sense of Gorla)
 \item The target behavioral equivalence is \emph{exact}
 \item Name invariance
 \item Operational correspondence (labeled version, assuming a generic renaming policy)
\end{enumerate}
\end{mydefi}

Using this definition of encoding, we state a separation result between \hop and \hocore.

\section{\hop cannot be encoded into \hocore}

\begin{myprop}
 There is no encoding of \hop into \hocore.
\end{myprop}

\begin{proof}[Sketch]
Suppose there is indeed an encoding $\encp{\cdot}{}$ of \hop into \hocore. Consider the following \hop process:
\[
  P_1 = a(x). \pu{a}{x} \parallel \Ho{a}{\overline{m} \parallel \overline{m}} 
%  P_2 = a(x). \pu{a}{\nil} \parallel \Ho{a}{\overline{m} \parallel \overline{m}} \quad
\]
Consider the encoding of $P_1$, taking into account compositionality:
%\begin{eqnarray*}
\[
\encp{P_1}{}  =  C^{\{a,m\}}_{\parallel}[\,C^{\{a\}}_{a(x)}[\,\encp{\pu{a}{x}}{}\,]\, , \, C^{\{m\}}_{\Ho{a}{\cdot}}[\, \encp{\overline{m} \parallel \overline{m}}{} \, ]\,] \\
\]
%\encp{P_2}{} & = & C^{\{a,m\}}_{\parallel}[\,C^{\{a\}}_{a(x)}[\,\encp{\pu{a}{\nil}}{}\,]\, , \, C^{\{m\}}_{\Ho{a}{\cdot}}[\, %\encp{\overline{m} \parallel \overline{m}}{} \, ]\,]
%\end{eqnarray*}
also notice that 
$(*) = \encp{\overline{m} \parallel \overline{m}}{} = C^{\{m\}}_{\parallel}[\, \encp{\overline{m}}{} \, , \, \encp{\overline{m}}{} \,]$.
Using operational correspondence and compositionality, process $(*)$ is seen to have the folowing properties:

\begin{enumerate}
 \item It has two weak output transitions on $m$
\item Transitions on names different from $m$ are not posssible
\item If it has one barb on $m$, then it has the other barb on $m$ as well. (This should go as a separate result, which follows by compositionality.)
\end{enumerate}

Now, notice that 
\[
 P_1 \arro{~\tau~} \arro{\overline{m}} P'_1
\]
then, by operational correspondence, it must be the case that 
\[
 \encp{P_1}{} \Ar{\overline{m}} \approx \encp{P'_1}{} \, .
\]
(Actually the label on the weak action should be something like $\encp{\overline{m}}{}$ but for the moment we can simplify that.)

Let us analyse the origin of $\overline{m}$ in $ \encp{P_1}{}$. We have three contexts, and thus three cases to check.
\begin{enumerate}
 \item It cannot originate from the outermost context, because any process with the same free variables would produce the barb.
We then have that
\[
 C^{\{a,m\}}_{\parallel}[\,\cdot, \cdot\,] \not \Downarrow_{\overline{m}}
\]

\item It cannot originate in the context of the output on $a$ neither, because the outputs on $m$ are the communication objects of the output on $a$ and thus blocked. We then have that
\[
 C^{\{m\}}_{\Ho{a}{\cdot}}[\,\cdot\,] \not \Downarrow_{\overline{m}}
\]

\item Finally, it is easy to see that since $m \not \in \fn{C^{\{a\}}_{a(x)}}$, then
\[
 C^{\{a\}}_{a(x)}[\cdot] \not \Downarrow_{\overline{m}}
\]
\end{enumerate}
It must be then the case that $\overline{m}$ originates in $(*)$.  Property (3) of $(*)$ says that, necessarily there are two barbs on 
$\overline{m}$: once a barb on $\overline{m}$ takes place then a second barb on $\overline{m}$ must take place as well. There is, however, a derivative of the source process $P_1$ that has only one output barb on $m$:
\[
 P_1 \arro{~\tau~} \pu{a}{\overline{m} \parallel \overline{m}} \arro{ \overline{m}} \pu{a}{ \overline{m}} \arro{ \overline{a}} \Ho{}{ \overline{m}} \not \downarrow_{\overline{m}}.
\]
Since, as we have argued, in all cases $\encp{P_1}{}$ will exhibit precisely two weak output barbs on $m$, we arrive to a behavior of $P_1$ that $\encp{P_1}{}$ is not able to match, a contradiction.
\end{proof}

\begin{myrem}
The above proposition holds for \hocore and \hop with restriction.
\end{myrem}

\begin{myrem}
Does the above proof sketch apply for $\mathcal{E}$?
Yes, with the process $$P_{2} = e.a[\outC{m} \parallel \outC{m}] \parallel \outC{e}.\tilde{a}\{\mathbf{0}\}$$
We have
$P_{2} \arro{~\tau~} a[\outC{m} \parallel \outC{m}] \parallel \tilde{a}\{\mathbf{0}\} \arro{~\outC{m}~} a[\outC{m}] \parallel \tilde{a}\{\mathbf{0}\} \arro{~\tau~}  \mathbf{0} \not \downarrow_{\overline{m}}$.
\end{myrem}






\section{Encoding \hocore into $\mathcal{E}$ with restriction}

\begin{eqnarray*}
\encp{\outC{a}\langle P \rangle}{1} & = & (\nu k',k)(e[k'.!\outC{k}] \parallel a[k.\encp{P}{1}] \parallel a_{2}.\outC{k'}) \\
\encp{a(x).Q}{1} & = & \update{e_{y}}{\bullet_{y} \parallel \update{a_{x}}{\encp{Q}{1}}.\outC{a_{2}}} \\
\encp{x}{1} & = & \bullet_{x} 
\end{eqnarray*}

%\begin{myrem}
%An encoding of \hop follows from the above encoding (as \hop is \hocore plus the same localities in $\mathcal{E}$).
%\end{myrem}

\begin{myrem}
What is the relationship with Ambients?
\end{myrem}

\section{Encoding linear \evol{} into $\pi$ }
\input{encEtoPi}

\nocite{SchmittS04}
\bibliographystyle{splncs}
\bibliography{referen,DSbib}



\end{document}